;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Ihelpers
  (sig chrs-words->strings (words))
  (sig get-max (stocks currmax))
  (sig sum-list (list))
  (sig average-list (list))
  
  (con chrs-words->strings-returns-list
       (implies (and (consp words) (char-listp (car words)))
                (equal t (string-listp (chrs-words->strings words)))))
  (con get-max-returns-stock-data
       (implies (and (consp stocks) 
                     (consp currmax)
                     (stringp (caar stocks))
                     (natp (cadar stocks))
                     (stringp (car currmax))
                     (natp (cadr currmax)))
    (equal t (and (stringp (car (get-max stocks currmax))) 
                  (natp (cadr (get-max stocks currmax)))))))
  (con sum-list-returns-number
       (implies (and (consp list) (rational-listp list))
                (equal t (rationalp (sum-list list)))))
  (con average-list-returns-number
       (implies (and (consp list) (rational-listp list))
                (equal t (rationalp (average-list list))))))